es:ES, X:AbsInterface(Top). prior(X)  AbsInterface(E(X)) 

latex

Definitions

s = t, t  T, ES, AbsInterface(A), Type, , A, (e <loc e'), x:A  B(x), x:A. B(x), x:AB(x), P & Q, P  Q, P  Q, left + right, Void, case b of inl(x) => s(x) | inr(y) => t(y), e < e', <a, b>, Id, False, if b then t else f fi , (e < e'), let x,y = A in B(x;y), t.1, Top, , (x  l), x  dom(f), A c B, a:A fp B(a), strong-subtype(A;B), E(X), prior(X), X(e), e  X, b, P  Q, E, x:A. B(x), x.A(x), can-apply(f;x), do-apply(f;x), outl(x), inr x , f(a), isl(x), x:A.B(x), {x:A| B(x)} , Decision, True, inl x

Lemmas

true wf, false wf, isl wf, event system wf, top wf, es-E-interface wf, es-interface wf, member wf, es-local-pred wf, es-local-pred-property, es-E wf, assert wf